\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:ecl(${\it ds}$; ${\it da}$), $m$:$\mathbb{N}$, $L$:(event{-}info(${\it ds}$;${\it da}$) List).
\\[0ex](ecl{-}act(${\it ds}$; ${\it da}$; $m$; $x$)($L$))
\\[0ex]$\Rightarrow$ \=($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List), $n$:$\mathbb{N}$.\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\Rightarrow$ (ecl{-}halt(${\it ds}$; ${\it da}$; $x$)($n$,${\it L'}$)) $\Rightarrow$ ($L$ = ${\it L'}$))
\-
\end{tabbing}